Iof proof for Lemma sq stable squash:
1. P :
2.
(P)
P
by ((((BasicSquashHD 2)
CollapseTHEN (UnhideSinceSquashedConcl))
)
CollapseTHEN (
C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n)) (first_tok :t) inil_term)))
C.| 9,38 |
(P)
P
by ((((BasicSquashHD 2)
CollapseTHEN (UnhideSinceSquashedConcl)))
CollapseTHEN (
C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n)) (first_tok :t) inil_term)))
C.
| Definitions |  TT |